Verification of neural networks relies on activation functions being piecewise affine (pwa) -- enabling an encoding of the verification problem for theorem provers. In this paper, we present the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks within Coq using the library Coquelicot for real analysis. As a proof-of-concept, we construct the popular pwa activation function ReLU. We integrate our formalization into a Coq model of neural networks, and devise a verified transformation from a neural network N to a pwa function representing N by composing pwa functions that we construct for each layer. This representation enables encodings for proof automation, e.g. Coq's tactic lra -- a decision procedure for linear real arithmetic. Further, our formalization paves the way for integrating Coq in frameworks of neural network verification as a fallback prover when automated proving fails.

We present a tool for computing exact forward and backward reachable sets of deep neural networks with rectified linear unit (ReLU) activation. We then develop algorithms using this tool to compute invariant sets and regions of attraction (ROAs) for control systems with neural networks in the feedback loop. Our algorithm is unique in that it builds the reachable sets by incrementally enumerating polyhedral regions in the input space, rather than iterating layer-by-layer through the network as in other methods. When performing safety verification, if an unsafe region is found, our algorithm can return this result without completing the full reachability computation, thus giving an anytime property that accelerates safety verification. Furthermore, we introduce a method to accelerate the computation of ROAs in the case that deep learned components are homeomorphisms, which we find is surprisingly common in practice. We demonstrate our tool in several test cases. We compute a ROA for a learned van der Pol oscillator model. We find a control invariant set for a learned torque-controlled pendulum model. We also verify specific safety properties for multiple deep networks related to the ACAS Xu aircraft collision advisory system. Finally, we apply our algorithm to find ROAs for an image-based aircraft runway taxi problem. Algorithm source code: https://github.com/StanfordMSL/Neural-Network-Reach .

In this paper, the disjunctive and conjunctive lattice piecewise affine (PWA) approximations of explicit linear model predictive control (MPC) are proposed. The training data are generated uniformly in the domain of interest, consisting of the state samples and corresponding affine control laws, based on which the lattice PWA approximations are constructed. Re-sampling of data is also proposed to guarantee that the lattice PWA approximations are identical to explicit MPC control law in the unique order (UO) regions containing the sample points as interior points. Additionally, under mild assumptions, the equivalence of the two lattice PWA approximations guarantees that the approximations are error-free in the domain of interest. The algorithms for deriving statistically error-free approximation to the explicit linear MPC are proposed and the complexity of the entire procedure is analyzed, which is polynomial with respect to the number of samples. The performance of the proposed approximation strategy is tested through two simulation examples, and the result shows that with a moderate number of sample points, we can construct lattice PWA approximations that are equivalent to optimal control law of the explicit linear MPC.

Rectifier (ReLU) deep neural networks (DNN) and their connection with piecewise affine (PWA) functions is analyzed. The paper is an effort to find and study the possibility of representing explicit state feedback policy of model predictive control (MPC) as a ReLU DNN, and vice versa. The complexity and architecture of DNN has been examined through some theorems and discussions. An approximate method has been developed for identification of input-space in ReLU net which results a PWA function over polyhedral regions. Also, inverse multiparametric linear or quadratic programs (mp-LP or mp-QP) has been studied which deals with reconstruction of constraints and cost function given a PWA function.